Nuprl Lemma : cond_rel_exp_monotone 4,23

n:T:Type, P:(TProp), R1R2:(TTProp).
when PR1 => R2  R1 preserves P  when PR1^n => R2^n 
latex


DefinitionsAB, A, False, R^n, R preserves P, when PR1 => R2, Prop, ij, P  Q, x:AB(x), t  T, , i=j, x f y, Unit, P  Q, , b, b, x:AB(x), P & Q
Lemmasle wf, rel exp wf, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, cond rel implies wf, preserved by wf, nat wf, nat properties, ge wf

origin